import copy

Inf = "Inf"
inf = "-Inf"

class Range(object):
    #top = Range(inf, Inf)
    #bottom = Range(is_bottom = True)
    
    def __init__(self, low = inf, high= Inf, is_bottom = False):
        self.low = low
        self.high = high
        self.is_bottom = is_bottom
        
    @staticmethod
    def get_top():        
        return Range(inf, Inf)
        
    @staticmethod
    def get_bottom():        
        return Range(is_bottom = True)
        
    @staticmethod
    def _min(a,b):
        if a == inf or b == inf:
            return inf
        if a == Inf:
            return b
        if b == Inf:
            return a
        return min(a,b)
    
    @staticmethod
    def _max(a,b):
        if a == Inf or b == Inf:
            return Inf
        if a == inf:
            return b
        if b == inf:
            return a
        return max(a,b)
        
    def __or__(self, other):#meet
        if self.is_bottom or other.is_bottom:
            return Range.get_bottom()
        
        low = Range._max(self.low, other.low)
        high = Range._min(self.high, other.high)
        
        if low != Range._min(low, high):
            return Range.get_bottom()
        
        return Range(low, high)
        
    def __and__(self, other):#join
        if other.is_bottom:
            return copy.copy(self)
        
        if self.is_bottom:
            return copy.copy(other)
        
        return Range(Range._min(self.low, other.low), Range._max(self.high, other.high))
    
    def __add__(self, other):
        if self.low == inf or other.low == inf:
            low = inf
        else:
            low = self.low + other.low
        if self.high == Inf or other.high == Inf:
            high = Inf
        else:
            high = self.high + other.high
        return Range(low, high)
    
    @staticmethod
    def join(a, b):
        return a & b
    
    @staticmethod
    def meet(a, b):
        return a | b
        
    @staticmethod
    def widening(a, b):
        if a.is_bottom:
            return b
        if b.is_bottom:
            return a
        if a.low <= b.low:
            low = a.low
        else:
            low = inf
        if a.high >= b.high:
            high = a.high
        else:
            high = Inf            
        return Range(low, high)
        
    @staticmethod
    def narrowing(a, b):
        if a.is_bottom:
            return b
        
        if b.is_bottom:
            return a
        
        if a.low == inf:
            low = b.low
        else:
            low = a.low
        if a.high == Inf:
            high = b.high
        else:
            high = a.high            
        return Range(low, high)
        
    def __eq__(self, other):
        if self.is_bottom:
            return other.is_bottom
        if other.is_bottom:
            return False
        return self.low == other.low and self.high == other.high
    
    def __str__(self):
        if self.is_bottom:
            return "()"
        return "(" + str(self.low) + "," + str(self.high) + ")"

class State(dict):
    def __init__(self, *args):
        super(State, self).__init__(*args)
        self.default_val = Range.get_top()
        #self.is_bottom = False
        self.is_top = False
        
    @staticmethod
    def get_top():        
        res = State()
        #res.is_top = True
        return res
        
    @staticmethod
    def get_bottom():        
        res = State()
        res.default_val = Range.get_bottom()
        #res.is_bottom = True
        return res
        
    @staticmethod
    def _combine_macro(a, b, func, allow_expanssion = True):
        res = State()
        print "_combine_macro",a,b
        for key in a.keys():
            if b.has_key(key):
                res[key] = func(a[key], b[key])
            else:
                if allow_expanssion:
                    res[key] = func(a[key], b.default_val)
        for key in b.keys():
            if not a.has_key(key):
                if allow_expanssion:
                    res[key] = func(a.default_val, b[key])
        res.default_val = func(a.default_val, b.default_val)
        return res
    
    def __str__(self):
        s='{'
        for key in self.keys():
            s += "(%s:%s), "%(str(key), str(self[key]))
        s += '}'
        return s
    
    def fix(self):
        if Range.get_bottom() in self.values():
            return State.get_bottom()
        return self
    
    @staticmethod
    def join(a,b):
        return State._combine_macro(a, b, Range.join)
        
    @staticmethod
    def meet(a,b):
        return State._combine_macro(a, b, Range.meet)
    
    @staticmethod
    def widening(a,b):
        return State._combine_macro(a, b, Range.widening)
        
    @staticmethod
    def narrowing(a,b):
        return State._combine_macro(a, b, Range.narrowing)
        
    def __eq__(self, other):
        return self == other and self.default_val == other.default_val
 
bottom = State.get_bottom()  # artifricial bottomalue to avoid the need to know the set of used expressions
top = State.get_top()
iota= top

class Exp(object):
    def __init__(self):
        pass
    def evaluate(self, state):
        pass
    
class AddConstExp(Exp):
    def __init__(self, var, const):
        self.var = var
        self.const = const
    def evaluate(self, state):
        return state[self.var] + Range(self.const, self.const)
    
    def __str__(self):
        return str(self.var) + " + " + str(self.const)
        
class ConstExp(Exp):
    def __init__(self, const):
        self.const = const
    def evaluate(self, state):
        return Range(self.const, self.const)
    def __str__(self):
        return str(self.const)
  
class ScanfExp(Exp):
    def __init__(self):
        pass
    def evaluate(self, state):
        return Range.get_top()
    def __str__(self):
        return "scanf"

def assign(state, var, e):
    print state
    print "assign",var,"=",e
    print "assign:",var,"=",e.evaluate(state)
    new_state = copy.copy(state)
    print new_state
    new_state[var] = e.evaluate(state)
    return new_state.fix()
    
def force_range(state, var, range):
    new_state = copy.copy(state)
    new_state[var] = state[var] | range #meld
    return new_state.fix()

def force_less(state, little, big, equal = False):
    new_state = copy.copy(state)
    if not state.has_key(little):
        new_state[little] = new_state.default_val
    if not state.has_key(big):
        new_state[big] = new_state.default_val
        
    if new_state[big].high == Inf:
        new_state[little] = new_state[little] | Range.get_top()
    elif new_state[big].high == inf:
        new_state[little] = new_state[little] | Range.get_bottom()
    else:
        new_state[little] = new_state[little] | Range(inf, state[big].high - 1 + 1*equal)
        
    if new_state[little].low == inf:
        new_state[big] = new_state[big] | Range.get_top()
    elif state[little].low == Inf:
        new_state[big] = new_state[big] | Range.get_bottom()
    else:
        new_state[big] = new_state[big] | Range(new_state[little].low  + 1 - 1*equal, Inf)
    return new_state.fix()

def force_exclude_from_range(state, var, val):
    new_state = copy.copy(state)
    
    if new_state[var].low == val:
        new_state[var].low += 1
        
    if new_state[var].high == val:
        new_state[var].high -= 1
    
    if new_state[var].high != Range._max(new_state[var].low, new_state[var].high):
        new_state[var] = Range.get_bottom()
        
    return new_state.fix()

